We present a tutorial on a simple imperative while language, and demonstrates how to statically analyze programs written in it using Codex, a modular abstract interpretation library. This also serves as a nice introduction to various codex components (Lattices, Single_value_abstraction, Domains...). It is mostly meant for developers who wish to use and extend Codex.
if and while). It also provides a concrete interpreter for the while language;Lattices and Single_value_abstraction with simpler implementations;